locl(a) sends [tg,f{AT}(x)] on link l once
== (subtype_rel(es-vartype(es; source(l); x); A)
==  (e:es-E(es). (es-kind(es; e) = rcv(l,tg))  subtype_rel(es-valtype(es; e); T)))
== c (e:es-E(es)
== c (((es-kind(es; e) = rcv(l,tg))
== c (c ((es-val(es; e) = f(es-when(es; x; es-sender(es; e))))
== c (c  (es-kind(es; es-sender(es; e)) = locl(a))
== c (c  (e':es-E(es). 
== c (c  (es-kind(es; e') = rcv(l,tg))
== c (c   (es-kind(es; es-sender(es; e')) = locl(a))
== c (c   (e' = e))))) 

latex

---

clarification:

send-once-p(es;T;A;a;l;tg;f;x)
== (subtype_rel(es-vartype(es; source(l); x); A)
==  (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  subtype_rel(es-valtype(es; e); T)))
== c (e:es-E(es)
== c (((es-kind(es; e) = rcv(l,tg)  Knd)
== c (c ((es-val(es; e) = f(es-when(es; x; es-sender(es; e)))  T)
== c (c  (es-kind(es; es-sender(es; e)) = locl(a)  Knd)
== c (c  (e':es-E(es). 
== c (c  (es-kind(es; e') = rcv(l,tg)  Knd)
== c (c   (es-kind(es; es-sender(es; e')) = locl(a)  Knd)
== c (c   (e' = e  es-E(es)))))) 

latex

Definitions	es-vartype(es; i; x), source(l), es-valtype(es; e), x:A. B(x), A c B, es-val(es; e), f(a), es-when(es; x; e), P  Q, x:A. B(x), rcv(l,tg), P  Q, Knd, es-kind(es; e), es-sender(es; e), locl(a), s = t, es-E(es)
FDL editor aliases	send-once-p